\documentclass[xcolor=dvipsnames,mathserif,svgnames,11pt]{beamer}

% for a handout:
%
%\documentclass[handout,11pt]{beamer}
%
%\usepackage{pgfpages}
%\pgfpagesuselayout{2 on 1}[letterpaper,border shrink=5mm]


\usepackage{diagrams}
\usepackage{listings}
\usepackage{proof}
\lstdefinelanguage{MyHaskell}
{alsoletter={+,|,->, =, ::}, morekeywords={+,|,->, =, ::, data, Int, max, case, of}
}


\lstdefinelanguage{MyLambda}
{alsoletter={\., |, ->, = }, morekeywords={=,|, -> ,\., lam , fix, case, of}}


%\lstset{language=MyHaskell, keywordstyle=\color{scyan},basicstyle=\ttfamily}

\definecolor{syellow}{RGB}{181,137,0}
\definecolor{scyan}{RGB}{42,161,152}

\DefineNamedColor{named}{MyBlue}{RGB}{38,139,210}
\DefineNamedColor{named}{Base3}{RGB}{253,246,227}
\DefineNamedColor{named}{Base00}{RGB}{101,123,131}
\newcommand{\cemph}[1]{\textcolor{Blue}{#1}}
\newcommand{\remph}[1]{\textcolor{Blue}{#1}}
\newcommand{\uemph}[1]{\underline{#1}}
\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\nat}[0]{\mathsf{Nat}} 
\newcommand{\ind}[0]{\mathsf{Ind}} 
\newcommand{\app}[0]{\mathsf{app}} 
\newcommand{\rec}[0]{\mathsf{rec}} 
\newcommand{\case}[0]{\mathsf{case}} 
\newcommand{\eq}[0]{\mathsf{Eq}} 
\newcommand{\add}[0]{\mathsf{add}} 

%% \newarrowfiller{dasheq} {==}{==}{==}{==}
%% \newarrow {Mapsto} |--->
%% \newarrow {Line} -----
%% \newarrow {Implies} ===={=>}
%% \newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
%% \newarrow {Onto} ----{>>}
%% \newarrow {Dashto}{}{dash}{}{dash}{>}
%% \newarrow {Dashtoo}{}{dash}{}{dash}{>>}

\include{seppp_annotated}
\mode<presentation>
{
  %\usetheme{Warsaw}
  % or ...
%gets rid of bottom navigation bars
%\setbeamertemplate{footline}[page number]{}

%gets rid of navigation symbols
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
\usetheme{default}
%\usecolortheme[named=MyBlue]{structure}
%\setbeamercolor{background canvas}{bg=Base3}
%\setbeamercolor{normal text}{fg=Base00}

%\usetheme{Edinburgh}

%  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}

\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.

\title[DTP13]
{Scott Encodings with Dependent Type and Self Type}

\author{Peng Fu, Aaron Stump}

\institute[University of Iowa]
{  
  Dept. of Computer Science\\ }
\date{}
%\date{May 22, 2013 }
% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}



% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
%\AtBeginSubsection[]
%{
%  \begin{frame}<beamer>
%    \frametitle{Outline}
%    \tableofcontents[currentsection,currentsubsection]
%  \end{frame}
%}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}

\begin{document}

\begin{frame}[plain]
  \titlepage
\end{frame}

\begin{frame}[fragile]
\frametitle{Inductive(Algebraic) Data types}

An example in Haskell: 

\begin{lstlisting}[language=MyHaskell, keywordstyle=\color{Blue},basicstyle=\ttfamily]
data Nat = Zero
          | Succ Nat

add :: Nat-> Nat -> Nat
add n m = case n of
          Zero -> m
         | Succ p -> add p (Succ m)

data List a = Nil | Cons a (List a)
data Tree = Empty
          | Leaf Int
          | Node Tree Tree
\end{lstlisting}

\end{frame}

\begin{frame}
\frametitle{Core Language Design}
To support (algebraic) data type, one way is 
to add data type and pattern matching(to core) as primitive.
\begin{itemize}
\item<1-> expression for data type declaration:

$\mathsf{data}\ T\ (a_i:A_i)_{i\in I}: A\ \mathsf{where}\ \{ C_i:A_i\}_{i\in I}$
\item<1-> expression for pattern matching :

$\mathsf{case} \ a\ \mathsf{of} \ \{ C_i (x_1,...x_u)\ \Rightarrow\ a \}_{i\in I}$

\item<2-> Now typing rule become: 

{\tiny $\SepppdruleTBXXBranch{}$}

\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Core Language Design}


\begin{itemize}
\item<1-> Complicated typing rules leads to complicate meta-theory. 
\item<2-> \textit{The machine-assisted proof of programming language properties}, 1996, Ph.D thesis by M. 
VanInwegen. 

\

Quoted from abstract: 

``We were not able to complete the proof of
type preservation because it is not true: we found counterexamples.''


\item<3-> In Haskell Core Language \footnote{http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/CoreSynType}: 

``Case expressions are the most complicated bit of Core. '' 

\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{  Scott Numerals}

\begin{itemize}

\item<1-> Scott encoding with Recursive Definition: 
\begin{lstlisting}[language=MyLambda, keywordstyle=\color{Blue},basicstyle=\ttfamily]
 Zero = lam s . lam z . z
 Succ n =  lam s . lam z . s n
 add n m = case n of 
              Zero -> m
            | Succ p -> add p (Succ m)
 pred n  = case n of 
              Zero -> Zero
            | Succ p -> p

\end{lstlisting}
\item<2-> Translate to lambda calculus with recursive definition

$\mathsf{Zero}\ := \lambda s.\lambda z.z$

$\mathsf{Succ}\ := \lambda n. \lambda s.\lambda z.s\ n$

$\mathsf{add}\ := \lambda n.\lambda m. n\ (\lambda p. \mathsf{add}\ p\ (\mathsf{Succ}\ m))\ m$

$\mathsf{pred}\ := \lambda n. n\ (\lambda p. p)\ \mathsf{Zero}$
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Scott Numerals}

\begin{itemize}
\item<1-> Isn't it great? No primitive data type and pattern matching needed!
\item<2-> Beta reduction and definition unfolding are enough.
\item<3-> The catch: Does not quite scale to dependent type programming. 

  \noindent E.g. One can not write a term of type $\Pi x:\mathsf{Nat}. \mathsf{add} \ x \ 0 =_{\mathsf{Nat}} x$, given $t_1 =_A t_2$ denotes $\Pi C: A \to *. C\ t_1 \to C\ t_2$. 
  
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Scott Numerals to Self Type}
\noindent $\Pi x:\mathsf{Nat}. \mathsf{add} \ x \ 0 =_{\mathsf{Nat}} x$, given $t_1 =_A t_2$ denotes $\Pi C: A \to *. C\ t_1 \to C\ t_2$. 

\noindent Assume $\nat := \Pi U:*. (\nat \to U) \to U \to U$.
\begin{itemize}
\item We need a term of type $\Pi U: \nat \to *. (\Pi y:\nat. U\ (\suc y)) \to U \ 0 \to \Pi x: \nat.U\ x$.
\item Given $\Gamma =  U:\nat \to *, s:\Pi y:\nat. U\ (\suc y), z:U\ 0, x:\nat $, can not construct a term of type $U\ x$. 
\item<2-> The idea: refine to $\nat := \Pi U:\nat \to *. (\Pi y:\nat. U\ (\suc y)) \to U\ 0 \to U\ \{?\}$.
\item<3-> The idea: refine to $\nat := \iota \cemph{x}.\Pi U:\nat \to *. (\Pi y:\nat. U\ (\suc y)) \to U\ 0 \to U\ \cemph{x}$.
 
\end{itemize}
\end{frame}



\begin{frame}
\frametitle{$\mathsf{Selfstar}$: I}
Given $\Gamma =  U:\nat \to *, s:\Pi y:\nat. U\ (\suc y), z:U\ 0, x:\nat $, can not construct a term of type $U\ x$. 

\begin{itemize}
\item add two typing rules: 

  \begin{tabular}{ll}
\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma
\vdash t : \iota x.T}


&
\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.T}{\Gamma
\vdash t: [t/x]T}
\\    
\end{tabular}
  \item Now $\case:= \lambda U.\lambda s.\lambda z.\lambda x.x\ U\ s\ z$ with 

    $\case: \Pi U: \nat \to *. (\Pi y:\nat. U\ (\suc y)) \to U \ 0 \to \Pi x: \nat.U\ x$.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{$\mathsf{Selfstar}$: II}
Scott encoding in $\mathsf{Selfstar}$
\begin{itemize}

\item Scott encoding($\tilde{\mu_s}$):

\noindent $(\remph{\mathsf{Nat}:*} ) \mapsto \iota x. \Pi C: \mathsf{Nat} \to *.  (\Pi n : \mathsf{Nat}.C\ (\mathsf{S}\ n)) \to (C\ 0) \to (C\ x)$

\noindent $(\remph{\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat}} )\mapsto \lambda n.\lambda C. \lambda s.\lambda z. s \ n$

\noindent $(\remph{0:\mathsf{Nat}})  \mapsto \lambda C. \lambda s. \lambda z.z$

\item Case analysis principle for Scott encoding:

\noindent $\tilde{\mu_s} \vdash (\remph{\mathsf{Case}}\ := \lambda C. \lambda s.\lambda z. \lambda n. n\ C\ s\ z):$

\noindent $ \Pi C: \mathsf{Nat} \to *. \Pi n:\mathsf{Nat}. (C\ (\mathsf{S}\ n)) \to C\ 0 \to \Pi n:\mathsf{Nat}. C\ n$

\item addition function:

$(\remph{\mathsf{add}: \mathsf{Nat} \to \mathsf{Nat} \to \mathsf{Nat}} ) \mapsto \lambda n.\lambda m. \mathsf{Case}\ (\lambda n.\mathsf{Nat})\ \ (\lambda p . (\mathsf{S}\ (\mathsf{add}\ p\ m)) )\ m\ n $ 

\end{itemize}  
\end{frame}


\begin{frame}
\frametitle{Summary}

\begin{itemize}
\item We seen Church and Scott encoding data and as alternatives to 
implement algebraic data type.
\item The use of confluence in preservation proof.
\item Several methods to prove confluence.
\item Limits of dependent type system give rise to $\mathsf{Selfstar}$. 
\item Introduced $\mathsf{Selfstar}$. 

\end{itemize}  
\end{frame}

\begin{frame}
\frametitle{Thank you for listening!}

\begin{itemize}
\item Questions? 
\end{itemize}  
\end{frame}


\end{document}



